Inference at * 
Iof proof for Lemma fseg wf:


  T:Type, L1, L2:(T List). fseg(T;L1;L2)   

latex

 by ((Unfold `fseg` ( 0)) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	fseg(T;L1;L2), x:A. B(x), x:A  B(x), , as @ bs, x:A. B(x), x:AB(x), type List, s = t, t  T, Type
Lemmas	append wf